\begin{tabbing}
$\forall$\=$T$:Type, $l$:IdLnk, ${\it ds}_{1}$, ${\it ds}_{2}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}_{1}$)$\rightarrow\mathbb{N}\rightarrow$Prop),\+
\\[0ex]$Q$:(State(${\it ds}_{2}$)$\rightarrow\mathbb{N}\rightarrow$Prop), $f$:(State(${\it ds}_{1}$)$\rightarrow\mathbb{N}\rightarrow$$T$).
\-\\[0ex]Normal($T$)
\\[0ex]$\Rightarrow$ Normal(${\it ds}_{1}$)
\\[0ex]$\Rightarrow$ Normal(${\it ds}_{2}$)
\\[0ex]$\Rightarrow$ $\neg$destination($l$) $=$ source($l$) $\in$ Id
\\[0ex]$\Rightarrow$ ($\forall$$s$:State(${\it ds}_{1}$). Dec($\exists$$k$:$\mathbb{N}$. $\neg$$P$($s$,$k$)))
\\[0ex]$\Rightarrow$ ($\forall$$s$:State(${\it ds}_{2}$). Dec($\exists$$k$:$\mathbb{N}$. $\neg$$Q$($s$,$k$)))
\\[0ex]$\Rightarrow$ ($\forall$$s$:State(${\it ds}_{1}$), $k$:$\mathbb{N}$. Dec($P$($s$,$k$)))
\\[0ex]$\Rightarrow$ ($\forall$$s$:State(${\it ds}_{2}$), $k$:$\mathbb{N}$. Dec($Q$($s$,$k$)))
\\[0ex]$\Rightarrow$ R{-}Feasible(sendMinimalR\=\{a:ut2, tg:ut2\}\+
\\[0ex]($T$; $l$; ${\it ds}_{1}$; ${\it ds}_{2}$; $P$; $Q$; $f$))
\-
\end{tabbing}